A:Type, eq:EqDecider(A), B:(AType), P:(A), f:x:A fp B(x), a:A.
((a  dom(f)))  (b:A. ((P(b)))  (b = a))  (fpf-vals(eq;P;f) ~ []) 

latex

Definitions	a:A fp B(a), let x = a in b(x), fpf-vals(eq;P;f), t  T, x:A. B(x), EqDecider(T), , x(s), x. t(x), Top, x  dom(f), b, A, , P  Q, P  Q, deq-member(eq;x;L), if b then t else f fi , filter(P;l), no_repeats(T;l), P  Q, (x  l), b, P & Q, Unit, False, P  Q, {T}, remove-repeats(eq;L), SQType(T), i  j , ||as||
Lemmas	length wf1, non neg length, filter wf, remove-repeats property, remove-repeats wf, nil member, false wf, cons member, no repeats wf, no repeats cons, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bnot wf, l member wf, iff wf, not wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, bool wf, deq wf